$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $f$:$x$:$A$ fp$\rightarrow$ $B$($x$), $C$:Type, $a$:($A$$\rightarrow$($C$+Unit)), $b$:($C$$\rightarrow$$A$), $y$:$C$.
\\[0ex]($y$ $\in$ fpf{-}domain(compose{-}fpf($a$;$b$;$f$)))
\\[0ex]$\Leftrightarrow$
\\[0ex]($\exists$$x$:$A$. ($x$ $\in$ fpf{-}domain($f$)) \& isl($a$($x$)) \& $y$ $=$ outl($a$($x$)))